(set-logic BV)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const bv_19-0 (_ BitVec 19))
(assert (not (forall ((q0 Bool) (q1 (_ BitVec 19)) (q2 (_ BitVec 19))) (=> (and v0 v6 v13 q0 q0 v9 q0) (distinct q1 q2)))))
(assert (not (exists ((q3 (_ BitVec 19)) (q4 Bool) (q5 Bool)) (distinct v8 v9 v18 v1 v6))))
(assert (or (forall ((q3 (_ BitVec 19)) (q4 Bool) (q5 Bool)) v9) (exists ((q3 (_ BitVec 19)) (q4 Bool) (q5 Bool)) (not (distinct bv_19-0 q3 q3 q3)))))
(declare-const v19 Bool)
(assert (not (exists ((q6 Bool) (q7 Bool) (q8 Bool) (q9 (_ BitVec 19))) (=> (= q9 q9 q9 bv_19-0 q9) (= q6 v12 q7 v9 q7 q6 v18)))))
(assert (or v7 v9 v4 (distinct v13 v17 v5 v12 v17 v1 (distinct v8 v9 v18 v1 v6))))
(declare-const v20 Bool)
(assert (not v14))
(declare-const v21 Bool)
(assert (= v5 v21 (or v7 v9 v4 (distinct v13 v17 v5 v12 v17 v1 (distinct v8 v9 v18 v1 v6))) v17 (not v14) v13 v8 v5 v12))
(assert (not (exists ((q10 (_ BitVec 12)) (q11 Bool)) v3)))
(assert (=> v4 (= #x2cf #x2cf #x149)))
(declare-const v22 Bool)
(declare-const v23 Bool)
(declare-const bv_1-0 (_ BitVec 1))
(assert (not (exists ((q12 (_ BitVec 19))) (not (bvsge (bvmul bv_19-0 bv_19-0) q12)))))
(declare-const bv_22-0 (_ BitVec 22))
(assert (exists ((q13 Bool) (q14 (_ BitVec 1)) (q15 (_ BitVec 19)) (q16 (_ BitVec 1))) v7))
(check-sat)